COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	facts about lengths of lists
C00004 00003	proofs lengthprop
C00005 ENDMK
C⊗;
;facts about lengths of lists
;10s
(wipe-out)
(get-proofs reverse prf ekl sys)
(get-proofs natnum prf ekl sys)

(proof lengthrev)

(decl length (type: |ground→ground|) (unaryname: length))
(define length |∀u x.(length nil=0)∧length(x.u)=(length u)'|
	(use listinductiondef))
(label simpinfo) (label lengthdef)

(axiom |∀u.natnum(length u)|)
(label simpinfo)

(axiom |∀u.length u=0≡null u|)
(label simpinfo)

(axiom |∀u v.length (u*v)=length u+length v|)
(label lengthadd) (label simpinfo)

(axiom |∀x.length (x.nil)=1|)
(label simpinfo)
 
(axiom |∀u.length (reverse u)=length u|)
(label simpinfo) (label lengthrev)

(save-proofs lengthrev)
;proofs lengthprop
(proof lengthprop)

(ue (phi |λu.natnum length u|) listinduction (open length))
;∀U.NATNUM(LENGTH U)

(ue (phi |λu.(length u=0)≡null u|) listinduction
    (open length) (use zero_not_successor))
;∀U.LENGTH U=0≡NULL U

(ue (phi |λu.length(u*v)=length u+length v|) listinduction
    (open append length))
;∀U.LENGTH (U*V)=LENGTH U+LENGTH V

(trw |length(x.nil)| (open length))
;LENGTH (X.NIL)=1

(ue (phi |λu.length (reverse u)=length u|) listinduction
    (open reverse length) (use lengthadd mode: always))
;∀U.LENGTH (REVERSE U)=LENGTH U